i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da).
Normal(ds)
 Normal(da)
 (kecl-kinds(A). (isrcv(k)  i = destination(lnk(k))  Id) & k  dom(da))
 "ecl"  dom(ds)
 ecl-machine1{ecl:ut2}
 ecl-machine1(i; ds; da; A)
 ||- es.es-decls(es;i;ds;da)
 ||- es. vartype(i;"ecl")  ecl-trans-type(ecl-trans(A))
 ||- es. & (n:.
 ||- es. & (e@i.
 ||- es. & (action[[A n]][es-init(es;e);e]
 ||- es. & (
 ||- es. & ((kind(e)  ecl-trans-ks(ecl-trans(A)))
 ||- es. & (& ecl-trans-a(ecl-trans(A))(n,kind(e),(state when e),val(e),"ecl" when e)) 

latex

Definitions

x:A. B(x), Id, P  Q, P & Q, "$x", ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-trans-type(A), , ecl-trans-ks(v), ecl-trans-a(v), t  T, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), Normal(T), x. t(x), 1of(t), SQType(T), {T}, Prop, State(ds), Valtype(da;k), P  Q, A & B, P  Q, P  Q, state@i, e@i. P(e), A, ||as||, Y, ij, t  ...$L, AB, False, True, b, true, if b t else f fi, Top, let x,y,z = a in t(x;y;z), T, es-trans-state-from{i:l}(es;ks;g;z;e1;e2), ecl-trans-state(v;L), ecl-trans-state-from(v;z;L), ecl-trans-init(v), es-init(es;e), false, ecl-trans-act(ds;da;A), x:A. B(x), as @ bs, list_accum(x,a.f(x;a);y;l), es-hist{i:l}(es;e1;e2), map(f;as), es-info(es;e), event-info(ds;da), xL. P(x), ecl-trans-tuple{i:l}(ds;da), x(s), Dec(P), e  e' , Knd, (x  l), , Unit,

Lemmas

ecl-trans-property, event-info wf, ecl-kinds-ecl-trans, atom-free-ecl-trans-type, ecl-trans wf, ecl-trans-tuple wf, R-state-var-init-rule, fpf-compatible-single, Knd sq, length wf1, non neg length, le wf, cons one one, l member wf, ecl-trans-ks wf, assert wf, isrcv wf, R-implies-rule, R-state-var-init wf, nat wf, iff wf, ecl-act wf, ecl-trans-act wf, atom-free wf, ecl-trans-type wf, not wf, fpf-dom wf, Id wf, id-deq wf, fpf-trivial-subtype-top, l all wf, Knd wf, ecl-kinds wf, ldst wf, lnk wf, Kind-deq wf, normal-da wf, normal-ds wf, ecl wf, fpf wf, es-decls-iff, alle-at wf, es-bact wf, es-isrcv wf, es-init wf, es-loc-init, es-state-when wf, subtype rel dep function, es-vartype wf, fpf-cap wf, top wf, subtype rel self, es-when wf, ecl-es-act-ecl-act, es-loc wf, es-E wf, iff functionality wrt iff, es-hist wf, assert-es-bact, decidable assert, es-first wf, bool cases, bool sq, bool wf, eqtt to assert, iff transitivity, bnot wf, eqff to assert, assert of bnot, es-interval-eq, es-info wf, es-kind wf, length nil, length cons, append wf, length append, es-interval-less-sq, es-init-le, es-first-init, map append sq, es-interval wf, es-pred wf, general-append-cancellation, es-loc-pred, deq wf, ecl-trans-state wf, es-after-pred, subtype rel wf, squash wf, true wf, event system wf, es-interval-eq2, decl-state wf, es-hist-last